$\forall$$T$:Type, ${\it as}$, ${\it bs}$:($T$ List). nth\_tl($\parallel$${\it as}$$\parallel$;${\it as}$ @ ${\it bs}$) $\sim$ ${\it bs}$